from z3 import *
variables = {
	'/myhouse.eprice': Real('/myhouse.eprice'),
	'/myhouse.time': Int('/myhouse.time'),
	'/myhouse.outtemp': Real('/myhouse.outtemp'),
	'/myhouse/room#liv.temp': Real('/myhouse/room#liv.temp'),
	'/myhouse/room#liv.bright': Real('/myhouse/room#liv.bright'),
	'/myhouse/room#liv.air': Int('/myhouse/room#liv.air'),
	'/myhouse/room#liv/window#w1.curtainOn': Bool('/myhouse/room#liv/window#w1.curtainOn'),
	'/myhouse/room#liv/window#w1.opened': Bool('/myhouse/room#liv/window#w1.opened'),
	'/myhouse/room#liv/window#w2.curtainOn': Bool('/myhouse/room#liv/window#w2.curtainOn'),
	'/myhouse/room#liv/window#w2.opened': Bool('/myhouse/room#liv/window#w2.opened'),
	'/myhouse/room#liv/heating#h1.level': Int('/myhouse/room#liv/heating#h1.level'),
	'/myhouse/room#liv/heating#h2.level': Int('/myhouse/room#liv/heating#h2.level'),
	'/myhouse/room#liv/light#0.level': Int('/myhouse/room#liv/light#0.level'),
	'/myhouse/room#liv/light#1.level': Int('/myhouse/room#liv/light#1.level'),
	'/myhouse/room#liv/ac#0.level': Int('/myhouse/room#liv/ac#0.level'),
	'/myhouse/room#liv/ac#0.freshAir': Bool('/myhouse/room#liv/ac#0.freshAir'),
	'/myhouse/room#liv/projector.on': Bool('/myhouse/room#liv/projector.on'),
	'/myhouse/room#liv/projector.brightness': Int('/myhouse/room#liv/projector.brightness'),
	'/myhouse/room#liv/projector.volume': Int('/myhouse/room#liv/projector.volume'),
	'/myhouse/room#liv/cm.loaded': Bool('/myhouse/room#liv/cm.loaded'),
	'/myhouse/room#liv/cm.on': Bool('/myhouse/room#liv/cm.on'),
	'/myhouse/room#liv/cm.warming': Bool('/myhouse/room#liv/cm.warming'),
	'/myhouse/room#kitchen.temp': Real('/myhouse/room#kitchen.temp'),
	'/myhouse/room#kitchen.bright': Real('/myhouse/room#kitchen.bright'),
	'/myhouse/room#kitchen.air': Int('/myhouse/room#kitchen.air'),
	'/myhouse/room#kitchen/light#0.level': Int('/myhouse/room#kitchen/light#0.level'),
	'/myhouse/room#kitchen/cooker.on': Bool('/myhouse/room#kitchen/cooker.on'),
	'/myhouse/room#kitchen/cm.loaded': Bool('/myhouse/room#kitchen/cm.loaded'),
	'/myhouse/room#kitchen/cm.on': Bool('/myhouse/room#kitchen/cm.on'),
	'/myhouse/room#kitchen/cm.warming': Bool('/myhouse/room#kitchen/cm.warming'),
	'/myhouse/room#bed1.temp': Real('/myhouse/room#bed1.temp'),
	'/myhouse/room#bed1.bright': Real('/myhouse/room#bed1.bright'),
	'/myhouse/room#bed1.air': Int('/myhouse/room#bed1.air'),
	'/myhouse/room#bed1/window#w1.curtainOn': Bool('/myhouse/room#bed1/window#w1.curtainOn'),
	'/myhouse/room#bed1/window#w1.opened': Bool('/myhouse/room#bed1/window#w1.opened'),
	'/myhouse/room#bed1/heating#h.level': Int('/myhouse/room#bed1/heating#h.level'),
	'/myhouse/room#bed1/light#0.level': Int('/myhouse/room#bed1/light#0.level'),
	'/myhouse/room#bed1/ac#0.level': Int('/myhouse/room#bed1/ac#0.level'),
	'/myhouse/room#bed1/ac#0.freshAir': Bool('/myhouse/room#bed1/ac#0.freshAir'),
	'/myhouse/room#bed2.temp': Real('/myhouse/room#bed2.temp'),
	'/myhouse/room#bed2.bright': Real('/myhouse/room#bed2.bright'),
	'/myhouse/room#bed2.air': Int('/myhouse/room#bed2.air'),
	'/myhouse/room#bed2/window#w1.curtainOn': Bool('/myhouse/room#bed2/window#w1.curtainOn'),
	'/myhouse/room#bed2/window#w1.opened': Bool('/myhouse/room#bed2/window#w1.opened'),
	'/myhouse/room#bed2/heating#h.level': Int('/myhouse/room#bed2/heating#h.level'),
	'/myhouse/room#bed2/light#0.level': Int('/myhouse/room#bed2/light#0.level'),
	'/myhouse/room#bed2/ac#0.level': Int('/myhouse/room#bed2/ac#0.level'),
	'/myhouse/room#bed2/ac#0.freshAir': Bool('/myhouse/room#bed2/ac#0.freshAir'),
	'/myhouse/room#family.temp': Real('/myhouse/room#family.temp'),
	'/myhouse/room#family.bright': Real('/myhouse/room#family.bright'),
	'/myhouse/room#family.air': Int('/myhouse/room#family.air'),
	'/myhouse/room#family/window#w1.curtainOn': Bool('/myhouse/room#family/window#w1.curtainOn'),
	'/myhouse/room#family/window#w1.opened': Bool('/myhouse/room#family/window#w1.opened'),
	'/myhouse/room#family/window#w2.curtainOn': Bool('/myhouse/room#family/window#w2.curtainOn'),
	'/myhouse/room#family/window#w2.opened': Bool('/myhouse/room#family/window#w2.opened'),
	'/myhouse/room#family/heating#h1.level': Int('/myhouse/room#family/heating#h1.level'),
	'/myhouse/room#family/heating#h2.level': Int('/myhouse/room#family/heating#h2.level'),
	'/myhouse/room#family/light#0.level': Int('/myhouse/room#family/light#0.level'),
	'/myhouse/room#family/ac#0.level': Int('/myhouse/room#family/ac#0.level'),
	'/myhouse/room#family/ac#0.freshAir': Bool('/myhouse/room#family/ac#0.freshAir'),
	'/myhouse/room#family/projector.on': Bool('/myhouse/room#family/projector.on'),
	'/myhouse/room#family/projector.brightness': Int('/myhouse/room#family/projector.brightness'),
	'/myhouse/room#family/projector.volume': Int('/myhouse/room#family/projector.volume'),
	'/myhouse/room#family/wm.loaded': Bool('/myhouse/room#family/wm.loaded'),
	'/myhouse/room#family/wm.on': Bool('/myhouse/room#family/wm.on'),
	'/myhouse/room#bed3.temp': Real('/myhouse/room#bed3.temp'),
	'/myhouse/room#bed3.bright': Real('/myhouse/room#bed3.bright'),
	'/myhouse/room#bed3.air': Int('/myhouse/room#bed3.air'),
	'/myhouse/room#bed3/window#w1.curtainOn': Bool('/myhouse/room#bed3/window#w1.curtainOn'),
	'/myhouse/room#bed3/window#w1.opened': Bool('/myhouse/room#bed3/window#w1.opened'),
	'/myhouse/room#bed3/heating#h.level': Int('/myhouse/room#bed3/heating#h.level'),
	'/myhouse/room#bed3/light#0.level': Int('/myhouse/room#bed3/light#0.level'),
	'/myhouse/room#bath1.temp': Real('/myhouse/room#bath1.temp'),
	'/myhouse/room#bath1.bright': Real('/myhouse/room#bath1.bright'),
	'/myhouse/room#bath1.air': Int('/myhouse/room#bath1.air'),
	'/myhouse/room#bath1/heating#h1.level': Int('/myhouse/room#bath1/heating#h1.level'),
	'/myhouse/room#bath1/light#0.level': Int('/myhouse/room#bath1/light#0.level'),
	'/myhouse/wh.temp': Real('/myhouse/wh.temp'),
	'/myhouse/wh.on': Bool('/myhouse/wh.on'),
	'/myhouse/wh.boost': Bool('/myhouse/wh.boost'),
	'/myhouse/ev#donkey.pluged': Bool('/myhouse/ev#donkey.pluged'),
	'/myhouse/ev#donkey.level': Int('/myhouse/ev#donkey.level'),
	'/myhouse/ev#donkey.charging': Bool('/myhouse/ev#donkey.charging'),
	'/myhouse/ev#horse.pluged': Bool('/myhouse/ev#horse.pluged'),
	'/myhouse/ev#horse.level': Int('/myhouse/ev#horse.level'),
	'/myhouse/ev#horse.charging': Bool('/myhouse/ev#horse.charging'),
	'/myhouse/gate.outlocked': Bool('/myhouse/gate.outlocked'),
	'/myhouse/sec.on': Bool('/myhouse/sec.on')
}
config_para = [
	variables['/myhouse/room#liv/window#w1.curtainOn'],
	variables['/myhouse/room#liv/window#w1.opened'],
	variables['/myhouse/room#liv/window#w2.curtainOn'],
	variables['/myhouse/room#liv/window#w2.opened'],
	variables['/myhouse/room#liv/heating#h1.level'],
	variables['/myhouse/room#liv/heating#h2.level'],
	variables['/myhouse/room#liv/light#0.level'],
	variables['/myhouse/room#liv/light#1.level'],
	variables['/myhouse/room#liv/ac#0.level'],
	variables['/myhouse/room#liv/ac#0.freshAir'],
	variables['/myhouse/room#liv/projector.on'],
	variables['/myhouse/room#liv/projector.brightness'],
	variables['/myhouse/room#liv/projector.volume'],
	variables['/myhouse/room#liv/cm.on'],
	variables['/myhouse/room#liv/cm.warming'],
	variables['/myhouse/room#kitchen/light#0.level'],
	variables['/myhouse/room#kitchen/cooker.on'],
	variables['/myhouse/room#kitchen/cm.on'],
	variables['/myhouse/room#kitchen/cm.warming'],
	variables['/myhouse/room#bed1/window#w1.curtainOn'],
	variables['/myhouse/room#bed1/window#w1.opened'],
	variables['/myhouse/room#bed1/heating#h.level'],
	variables['/myhouse/room#bed1/light#0.level'],
	variables['/myhouse/room#bed1/ac#0.level'],
	variables['/myhouse/room#bed1/ac#0.freshAir'],
	variables['/myhouse/room#bed2/window#w1.curtainOn'],
	variables['/myhouse/room#bed2/window#w1.opened'],
	variables['/myhouse/room#bed2/heating#h.level'],
	variables['/myhouse/room#bed2/light#0.level'],
	variables['/myhouse/room#bed2/ac#0.level'],
	variables['/myhouse/room#bed2/ac#0.freshAir'],
	variables['/myhouse/room#family/window#w1.curtainOn'],
	variables['/myhouse/room#family/window#w1.opened'],
	variables['/myhouse/room#family/window#w2.curtainOn'],
	variables['/myhouse/room#family/window#w2.opened'],
	variables['/myhouse/room#family/heating#h1.level'],
	variables['/myhouse/room#family/heating#h2.level'],
	variables['/myhouse/room#family/light#0.level'],
	variables['/myhouse/room#family/ac#0.level'],
	variables['/myhouse/room#family/ac#0.freshAir'],
	variables['/myhouse/room#family/projector.on'],
	variables['/myhouse/room#family/projector.brightness'],
	variables['/myhouse/room#family/projector.volume'],
	variables['/myhouse/room#family/wm.on'],
	variables['/myhouse/room#bed3/window#w1.curtainOn'],
	variables['/myhouse/room#bed3/window#w1.opened'],
	variables['/myhouse/room#bed3/heating#h.level'],
	variables['/myhouse/room#bed3/light#0.level'],
	variables['/myhouse/room#bath1/heating#h1.level'],
	variables['/myhouse/room#bath1/light#0.level'],
	variables['/myhouse/wh.on'],
	variables['/myhouse/wh.boost'],
	variables['/myhouse/ev#donkey.charging'],
	variables['/myhouse/ev#horse.charging'],
	variables['/myhouse/sec.on']
]
context_para = [
	variables['/myhouse.eprice'],
	variables['/myhouse.time'],
	variables['/myhouse.outtemp'],
	variables['/myhouse/room#liv.temp'],
	variables['/myhouse/room#liv.bright'],
	variables['/myhouse/room#liv.air'],
	variables['/myhouse/room#liv/cm.loaded'],
	variables['/myhouse/room#kitchen.temp'],
	variables['/myhouse/room#kitchen.bright'],
	variables['/myhouse/room#kitchen.air'],
	variables['/myhouse/room#kitchen/cm.loaded'],
	variables['/myhouse/room#bed1.temp'],
	variables['/myhouse/room#bed1.bright'],
	variables['/myhouse/room#bed1.air'],
	variables['/myhouse/room#bed2.temp'],
	variables['/myhouse/room#bed2.bright'],
	variables['/myhouse/room#bed2.air'],
	variables['/myhouse/room#family.temp'],
	variables['/myhouse/room#family.bright'],
	variables['/myhouse/room#family.air'],
	variables['/myhouse/room#family/wm.loaded'],
	variables['/myhouse/room#bed3.temp'],
	variables['/myhouse/room#bed3.bright'],
	variables['/myhouse/room#bed3.air'],
	variables['/myhouse/room#bath1.temp'],
	variables['/myhouse/room#bath1.bright'],
	variables['/myhouse/room#bath1.air'],
	variables['/myhouse/wh.temp'],
	variables['/myhouse/ev#donkey.pluged'],
	variables['/myhouse/ev#donkey.level'],
	variables['/myhouse/ev#horse.pluged'],
	variables['/myhouse/ev#horse.level'],
	variables['/myhouse/gate.outlocked']
]
config = {
	'/myhouse/room#liv/window#w1.curtainOn': False,
	'/myhouse/room#liv/window#w1.opened': False,
	'/myhouse/room#liv/window#w2.curtainOn': False,
	'/myhouse/room#liv/window#w2.opened': True,
	'/myhouse/room#liv/heating#h1.level': 0,
	'/myhouse/room#liv/heating#h2.level': 7,
	'/myhouse/room#liv/light#0.level': 0,
	'/myhouse/room#liv/light#1.level': 3,
	'/myhouse/room#liv/ac#0.level': 0,
	'/myhouse/room#liv/ac#0.freshAir': False,
	'/myhouse/room#liv/projector.on': True,
	'/myhouse/room#liv/projector.brightness': 5,
	'/myhouse/room#liv/projector.volume': 6,
	'/myhouse/room#liv/cm.on': False,
	'/myhouse/room#liv/cm.warming': True,
	'/myhouse/room#kitchen/light#0.level': 3,
	'/myhouse/room#kitchen/cooker.on': True,
	'/myhouse/room#kitchen/cm.on': True,
	'/myhouse/room#kitchen/cm.warming': True,
	'/myhouse/room#bed1/window#w1.curtainOn': True,
	'/myhouse/room#bed1/window#w1.opened': True,
	'/myhouse/room#bed1/heating#h.level': 6,
	'/myhouse/room#bed1/light#0.level': 0,
	'/myhouse/room#bed1/ac#0.level': 0,
	'/myhouse/room#bed1/ac#0.freshAir': False,
	'/myhouse/room#bed2/window#w1.curtainOn': False,
	'/myhouse/room#bed2/window#w1.opened': True,
	'/myhouse/room#bed2/heating#h.level': 6,
	'/myhouse/room#bed2/light#0.level': 2,
	'/myhouse/room#bed2/ac#0.level': 0,
	'/myhouse/room#bed2/ac#0.freshAir': False,
	'/myhouse/room#family/window#w1.curtainOn': False,
	'/myhouse/room#family/window#w1.opened': False,
	'/myhouse/room#family/window#w2.curtainOn': False,
	'/myhouse/room#family/window#w2.opened': True,
	'/myhouse/room#family/heating#h1.level': 0,
	'/myhouse/room#family/heating#h2.level': 10,
	'/myhouse/room#family/light#0.level': 0,
	'/myhouse/room#family/ac#0.level': 0,
	'/myhouse/room#family/ac#0.freshAir': False,
	'/myhouse/room#family/projector.on': False,
	'/myhouse/room#family/projector.brightness': 5,
	'/myhouse/room#family/projector.volume': 9,
	'/myhouse/room#family/wm.on': False,
	'/myhouse/room#bed3/window#w1.curtainOn': True,
	'/myhouse/room#bed3/window#w1.opened': True,
	'/myhouse/room#bed3/heating#h.level': 0,
	'/myhouse/room#bed3/light#0.level': 0,
	'/myhouse/room#bath1/heating#h1.level': 10,
	'/myhouse/room#bath1/light#0.level': 3,
	'/myhouse/wh.on': True,
	'/myhouse/wh.boost': False,
	'/myhouse/ev#donkey.charging': False,
	'/myhouse/ev#horse.charging': True,
	'/myhouse/sec.on': False
}
context = {
	'/myhouse.eprice': 10.0,
	'/myhouse.time': 23,
	'/myhouse.outtemp': 12,
	'/myhouse/room#liv.temp': 9.0,
	'/myhouse/room#liv.bright': 4000.0,
	'/myhouse/room#liv.air': 0,
	'/myhouse/room#liv/cm.loaded': True,
	'/myhouse/room#kitchen.temp': 0.0,
	'/myhouse/room#kitchen.bright': 30.0,
	'/myhouse/room#kitchen.air': 6,
	'/myhouse/room#kitchen/cm.loaded': True,
	'/myhouse/room#bed1.temp': 15.0,
	'/myhouse/room#bed1.bright': 4000,
	'/myhouse/room#bed1.air': 7,
	'/myhouse/room#bed2.temp': 10.0,
	'/myhouse/room#bed2.bright': 2000,
	'/myhouse/room#bed2.air': 0,
	'/myhouse/room#family.temp': 20.0,
	'/myhouse/room#family.bright': 4000.0,
	'/myhouse/room#family.air': 0,
	'/myhouse/room#family/wm.loaded': True,
	'/myhouse/room#bed3.temp': 22.0,
	'/myhouse/room#bed3.bright': 500,
	'/myhouse/room#bed3.air': 8,
	'/myhouse/room#bath1.temp': 25.0,
	'/myhouse/room#bath1.bright': 2000,
	'/myhouse/room#bath1.air': 0,
	'/myhouse/wh.temp': 20,
	'/myhouse/ev#donkey.pluged': False,
	'/myhouse/ev#donkey.level': 90,
	'/myhouse/ev#horse.pluged': True,
	'/myhouse/ev#horse.level': 10,
	'/myhouse/gate.outlocked': False
}

goals = [
	Implies((variables['/myhouse.eprice']) > (20), And(And(And((variables['/myhouse/ev#donkey.charging']) == (False), (variables['/myhouse/ev#horse.charging']) == (False) ), Not(variables['/myhouse/wh.on'])), And((variables['/myhouse/room#bed2/heating#h.level']) == (0), (variables['/myhouse/room#liv/heating#h1.level']) == (0), (variables['/myhouse/room#liv/heating#h2.level']) == (0), (variables['/myhouse/room#bed3/heating#h.level']) == (0), (variables['/myhouse/room#family/heating#h1.level']) == (0), (variables['/myhouse/room#family/heating#h2.level']) == (0), (variables['/myhouse/room#bed1/heating#h.level']) == (0), (variables['/myhouse/room#bath1/heating#h1.level']) == (0) ))),
	Implies((variables['/myhouse.eprice']) > (15), Or(Or(And((variables['/myhouse/ev#donkey.charging']) == (False), (variables['/myhouse/ev#horse.charging']) == (False) ), Not(variables['/myhouse/wh.on'])), And((variables['/myhouse/room#bed2/heating#h.level']) < (3), (variables['/myhouse/room#liv/heating#h1.level']) < (3), (variables['/myhouse/room#liv/heating#h2.level']) < (3), (variables['/myhouse/room#bed3/heating#h.level']) < (3), (variables['/myhouse/room#family/heating#h1.level']) < (3), (variables['/myhouse/room#family/heating#h2.level']) < (3), (variables['/myhouse/room#bed1/heating#h.level']) < (3), (variables['/myhouse/room#bath1/heating#h1.level']) < (3) ))),
	Implies(variables['/myhouse/gate.outlocked'], variables['/myhouse/sec.on']),
	Implies(variables['/myhouse/sec.on'], And((variables['/myhouse/room#liv/window#w2.opened']) == (False), (variables['/myhouse/room#liv/window#w1.opened']) == (False) )),
	Implies((variables['/myhouse/room#liv.temp']) < (18), Or((variables['/myhouse/room#liv/heating#h1.level']) > (0), (variables['/myhouse/room#liv/heating#h2.level']) > (0) )),
	Implies((variables['/myhouse.time']) > (22), (variables['/myhouse/room#liv/projector.volume']) < (4)),
	Implies((variables['/myhouse/room#liv.temp']) < (10), (variables['/myhouse/room#liv/heating#h1.level'] + variables['/myhouse/room#liv/heating#h2.level']  ) > ((3) * (2))),
	Implies(And(variables['/myhouse/room#liv/projector.on'], (variables['/myhouse/room#liv.bright']) > (500)), And(And((variables['/myhouse/room#liv/light#1.level']) == (0), (variables['/myhouse/room#liv/light#0.level']) == (0) ), And(variables['/myhouse/room#liv/window#w2.curtainOn'], variables['/myhouse/room#liv/window#w1.curtainOn'] ))),
	Implies((variables['/myhouse/room#liv.air']) > (5), Or(variables['/myhouse/room#liv/window#w2.opened'], variables['/myhouse/room#liv/window#w1.opened'] )),
	Or(And((variables['/myhouse/room#liv/heating#h1.level']) == (0), (variables['/myhouse/room#liv/heating#h2.level']) == (0) ), And((variables['/myhouse/room#liv/ac#0.level']) == (0) )),
	Or(And((variables['/myhouse/room#liv/window#w2.opened']) == (False), (variables['/myhouse/room#liv/window#w1.opened']) == (False) ), And((variables['/myhouse/room#liv/ac#0.level']) == (0) )),
	Or((variables['/myhouse.outtemp']) > (5), And(Not(variables['/myhouse/room#liv/window#w2.opened']), Not(variables['/myhouse/room#liv/window#w1.opened']) )),
	Implies((variables['/myhouse/room#liv.temp']) < (23), (variables['/myhouse/room#liv/ac#0.level']) == (0)),
	Implies((variables['/myhouse/room#liv.temp']) > (28), (variables['/myhouse/room#liv/ac#0.level']) > (5)),
	Implies((variables['/myhouse.outtemp']) > (30), (variables['/myhouse/room#liv/ac#0.level']) > (5)),
	Implies(And((variables['/myhouse.time']) == (7), variables['/myhouse/room#liv/cm.loaded']), variables['/myhouse/room#liv/cm.on']),
	Implies((variables['/myhouse/room#liv.temp']) > (20), Not(variables['/myhouse/room#liv/cm.warming'])),
	Or(Or(variables['/myhouse/ev#donkey.pluged'], variables['/myhouse/ev#horse.pluged'] ), variables['/myhouse/room#liv/cm.on']),
	Implies((variables['/myhouse/room#kitchen.bright']) > (500), And((variables['/myhouse/room#kitchen/light#0.level']) == (0) )),
	Implies(And((variables['/myhouse.time']) == (7), variables['/myhouse/room#kitchen/cm.loaded']), variables['/myhouse/room#kitchen/cm.on']),
	Implies((variables['/myhouse/room#kitchen.temp']) > (20), Not(variables['/myhouse/room#kitchen/cm.warming'])),
	Or(Or(variables['/myhouse/ev#donkey.pluged'], variables['/myhouse/ev#horse.pluged'] ), variables['/myhouse/room#kitchen/cm.on']),
	Implies((variables['/myhouse/room#bed1.temp']) < (18), Or((variables['/myhouse/room#bed1/heating#h.level']) > (0) )),
	Implies((variables['/myhouse/room#bed1.temp']) < (10), (variables['/myhouse/room#bed1/heating#h.level']  ) > ((3) * (1))),
	Implies((variables['/myhouse/room#bed1.bright']) > (500), And(And((variables['/myhouse/room#bed1/light#0.level']) == (0) ), And(variables['/myhouse/room#bed1/window#w1.curtainOn'] ))),
	Implies((variables['/myhouse/room#bed1.air']) > (5), Or(variables['/myhouse/room#bed1/window#w1.opened'] )),
	Or(And((variables['/myhouse/room#bed1/heating#h.level']) == (0) ), And((variables['/myhouse/room#bed1/ac#0.level']) == (0) )),
	Or(And((variables['/myhouse/room#bed1/window#w1.opened']) == (False) ), And((variables['/myhouse/room#bed1/ac#0.level']) == (0) )),
	Or((variables['/myhouse.outtemp']) > (5), And(Not(variables['/myhouse/room#bed1/window#w1.opened']) )),
	Implies((variables['/myhouse/room#bed1.temp']) < (23), (variables['/myhouse/room#bed1/ac#0.level']) == (0)),
	Implies((variables['/myhouse/room#bed1.temp']) > (28), (variables['/myhouse/room#bed1/ac#0.level']) > (5)),
	Implies((variables['/myhouse.outtemp']) > (30), (variables['/myhouse/room#bed1/ac#0.level']) > (5)),
	Implies((variables['/myhouse/room#bed2.temp']) < (18), Or((variables['/myhouse/room#bed2/heating#h.level']) > (0) )),
	Implies((variables['/myhouse/room#bed2.temp']) < (10), (variables['/myhouse/room#bed2/heating#h.level']  ) > ((3) * (1))),
	Implies((variables['/myhouse/room#bed2.bright']) > (500), And(And((variables['/myhouse/room#bed2/light#0.level']) == (0) ), And(variables['/myhouse/room#bed2/window#w1.curtainOn'] ))),
	Implies((variables['/myhouse/room#bed2.air']) > (5), Or(variables['/myhouse/room#bed2/window#w1.opened'] )),
	Or(And((variables['/myhouse/room#bed2/heating#h.level']) == (0) ), And((variables['/myhouse/room#bed2/ac#0.level']) == (0) )),
	Or(And((variables['/myhouse/room#bed2/window#w1.opened']) == (False) ), And((variables['/myhouse/room#bed2/ac#0.level']) == (0) )),
	Or((variables['/myhouse.outtemp']) > (5), And(Not(variables['/myhouse/room#bed2/window#w1.opened']) )),
	Implies((variables['/myhouse/room#bed2.temp']) < (23), (variables['/myhouse/room#bed2/ac#0.level']) == (0)),
	Implies((variables['/myhouse/room#bed2.temp']) > (28), (variables['/myhouse/room#bed2/ac#0.level']) > (5)),
	Implies((variables['/myhouse.outtemp']) > (30), (variables['/myhouse/room#bed2/ac#0.level']) > (5)),
	Implies((variables['/myhouse/room#family.temp']) < (18), Or((variables['/myhouse/room#family/heating#h1.level']) > (0), (variables['/myhouse/room#family/heating#h2.level']) > (0) )),
	Implies((variables['/myhouse.time']) > (22), (variables['/myhouse/room#family/projector.volume']) < (4)),
	Implies((variables['/myhouse/room#family.temp']) < (10), (variables['/myhouse/room#family/heating#h1.level'] + variables['/myhouse/room#family/heating#h2.level']  ) > ((3) * (2))),
	Implies(And(variables['/myhouse/room#family/projector.on'], (variables['/myhouse/room#family.bright']) > (500)), And(And((variables['/myhouse/room#family/light#0.level']) == (0) ), And(variables['/myhouse/room#family/window#w2.curtainOn'], variables['/myhouse/room#family/window#w1.curtainOn'] ))),
	Implies((variables['/myhouse/room#family.air']) > (5), Or(variables['/myhouse/room#family/window#w2.opened'], variables['/myhouse/room#family/window#w1.opened'] )),
	Or(And((variables['/myhouse/room#family/heating#h1.level']) == (0), (variables['/myhouse/room#family/heating#h2.level']) == (0) ), And((variables['/myhouse/room#family/ac#0.level']) == (0) )),
	Or(And((variables['/myhouse/room#family/window#w2.opened']) == (False), (variables['/myhouse/room#family/window#w1.opened']) == (False) ), And((variables['/myhouse/room#family/ac#0.level']) == (0) )),
	Or((variables['/myhouse.outtemp']) > (5), And(Not(variables['/myhouse/room#family/window#w2.opened']), Not(variables['/myhouse/room#family/window#w1.opened']) )),
	Implies((variables['/myhouse/room#family.temp']) < (23), (variables['/myhouse/room#family/ac#0.level']) == (0)),
	Implies((variables['/myhouse/room#family.temp']) > (28), (variables['/myhouse/room#family/ac#0.level']) > (5)),
	Implies((variables['/myhouse.outtemp']) > (30), (variables['/myhouse/room#family/ac#0.level']) > (5)),
	Or(Not(variables['/myhouse/room#family/wm.on']), Not(variables['/myhouse/room#family/projector.on'])),
	Implies(variables['/myhouse/room#family/wm.loaded'], variables['/myhouse/room#family/wm.on']),
	Implies((variables['/myhouse/room#bed3.temp']) < (18), Or((variables['/myhouse/room#bed3/heating#h.level']) > (0) )),
	Implies((variables['/myhouse/room#bed3.temp']) < (10), (variables['/myhouse/room#bed3/heating#h.level']  ) > ((3) * (1))),
	Implies((variables['/myhouse/room#bed3.bright']) > (500), And(And((variables['/myhouse/room#bed3/light#0.level']) == (0) ), And(variables['/myhouse/room#bed3/window#w1.curtainOn'] ))),
	Implies((variables['/myhouse/room#bed3.air']) > (5), Or(variables['/myhouse/room#bed3/window#w1.opened'] )),
	And((variables['/myhouse/room#bed3/heating#h.level']) == (0) ),
	And((variables['/myhouse/room#bed3/window#w1.opened']) == (False) ),
	Or((variables['/myhouse.outtemp']) > (5), And(Not(variables['/myhouse/room#bed3/window#w1.opened']) )),
	Implies((variables['/myhouse/room#bath1.temp']) < (18), Or((variables['/myhouse/room#bath1/heating#h1.level']) > (0) )),
	Implies((variables['/myhouse/room#bath1.temp']) < (10), (variables['/myhouse/room#bath1/heating#h1.level']  ) > ((3) * (1))),
	Implies((variables['/myhouse/room#bath1.bright']) > (500), And((variables['/myhouse/room#bath1/light#0.level']) == (0) )),
	And((variables['/myhouse/room#bath1/heating#h1.level']) == (0) ),
	Or(Or((variables['/myhouse.time']) < (2), (variables['/myhouse.time']) > (8)), variables['/myhouse/wh.on']),
	Implies((variables['/myhouse/wh.temp']) < (30), variables['/myhouse/wh.on']),
	Or((variables['/myhouse/wh.temp']) < (50), Not(variables['/myhouse/wh.on'])),
	Implies((variables['/myhouse.eprice']) < (10), variables['/myhouse/ev#horse.charging']),
	Implies((variables['/myhouse/ev#horse.level']) < (30), variables['/myhouse/ev#horse.charging'])
]
domains = [
	And(variables['/myhouse/room#liv/heating#h1.level'] >= 0, variables['/myhouse/room#liv/heating#h1.level'] <= 10),
	And(variables['/myhouse/room#liv/heating#h2.level'] >= 0, variables['/myhouse/room#liv/heating#h2.level'] <= 10),
	And(variables['/myhouse/room#liv/light#0.level'] >= 0, variables['/myhouse/room#liv/light#0.level'] <= 10),
	And(variables['/myhouse/room#liv/light#1.level'] >= 0, variables['/myhouse/room#liv/light#1.level'] <= 10),
	And(variables['/myhouse/room#liv/ac#0.level'] >= 0, variables['/myhouse/room#liv/ac#0.level'] <= 10),
	And(variables['/myhouse/room#liv/projector.brightness'] >= 0, variables['/myhouse/room#liv/projector.brightness'] <= 10),
	And(variables['/myhouse/room#liv/projector.volume'] >= 0, variables['/myhouse/room#liv/projector.volume'] <= 10),
	And(variables['/myhouse/room#kitchen/light#0.level'] >= 0, variables['/myhouse/room#kitchen/light#0.level'] <= 10),
	And(variables['/myhouse/room#bed1/heating#h.level'] >= 0, variables['/myhouse/room#bed1/heating#h.level'] <= 10),
	And(variables['/myhouse/room#bed1/light#0.level'] >= 0, variables['/myhouse/room#bed1/light#0.level'] <= 10),
	And(variables['/myhouse/room#bed1/ac#0.level'] >= 0, variables['/myhouse/room#bed1/ac#0.level'] <= 10),
	And(variables['/myhouse/room#bed2/heating#h.level'] >= 0, variables['/myhouse/room#bed2/heating#h.level'] <= 10),
	And(variables['/myhouse/room#bed2/light#0.level'] >= 0, variables['/myhouse/room#bed2/light#0.level'] <= 10),
	And(variables['/myhouse/room#bed2/ac#0.level'] >= 0, variables['/myhouse/room#bed2/ac#0.level'] <= 10),
	And(variables['/myhouse/room#family/heating#h1.level'] >= 0, variables['/myhouse/room#family/heating#h1.level'] <= 10),
	And(variables['/myhouse/room#family/heating#h2.level'] >= 0, variables['/myhouse/room#family/heating#h2.level'] <= 10),
	And(variables['/myhouse/room#family/light#0.level'] >= 0, variables['/myhouse/room#family/light#0.level'] <= 10),
	And(variables['/myhouse/room#family/ac#0.level'] >= 0, variables['/myhouse/room#family/ac#0.level'] <= 10),
	And(variables['/myhouse/room#family/projector.brightness'] >= 0, variables['/myhouse/room#family/projector.brightness'] <= 10),
	And(variables['/myhouse/room#family/projector.volume'] >= 0, variables['/myhouse/room#family/projector.volume'] <= 10),
	And(variables['/myhouse/room#bed3/heating#h.level'] >= 0, variables['/myhouse/room#bed3/heating#h.level'] <= 10),
	And(variables['/myhouse/room#bed3/light#0.level'] >= 0, variables['/myhouse/room#bed3/light#0.level'] <= 10),
	And(variables['/myhouse/room#bath1/heating#h1.level'] >= 0, variables['/myhouse/room#bath1/heating#h1.level'] <= 10),
	And(variables['/myhouse/room#bath1/light#0.level'] >= 0, variables['/myhouse/room#bath1/light#0.level'] <= 10)
]
users = [
	(lambda cont,conf:cont['/myhouse/gate.outlocked']  , '/myhouse/sec.on', True),
	(lambda cont,conf:conf['/myhouse/room#liv/projector.on'] , '/myhouse/room#liv/window#w2.curtainOn', True),
	(lambda cont,conf: (cont['/myhouse/room#liv.air'] ) > (6) and (cont['/myhouse.outtemp'] ) >= (10)  , '/myhouse/room#liv/window#w2.opened', True),
	(lambda cont,conf: (cont['/myhouse/room#liv.temp'] ) < (10) and (cont['/myhouse.eprice'] ) < (20)  , '/myhouse/room#liv/heating#h1.level', 10),
	(lambda cont,conf:(conf['/myhouse/room#liv/light#0.level']) != (0) , '/myhouse/room#liv/light#0.level', 5),
	(lambda cont,conf:(conf['/myhouse/room#liv/light#1.level']) != (0) , '/myhouse/room#liv/light#1.level', 5),
	(lambda cont,conf:(conf['/myhouse/room#liv/ac#0.level']) > (0) , '/myhouse/room#liv/ac#0.level', 9),
	(lambda cont,conf:cont['/myhouse/room#liv/cm.loaded']  , '/myhouse/room#liv/cm.warming', True),
	(lambda cont,conf:(conf['/myhouse/room#kitchen/light#0.level']) != (0) , '/myhouse/room#kitchen/light#0.level', 5),
	(lambda cont,conf:cont['/myhouse/room#kitchen/cm.loaded']  , '/myhouse/room#kitchen/cm.warming', True),
	(lambda cont,conf: (cont['/myhouse/room#bed1.air'] ) > (6) and (cont['/myhouse.outtemp'] ) >= (10)  , '/myhouse/room#bed1/window#w1.opened', True),
	(lambda cont,conf: (cont['/myhouse/room#bed1.temp'] ) < (10) and (cont['/myhouse.eprice'] ) < (20)  , '/myhouse/room#bed1/heating#h.level', 10),
	(lambda cont,conf:(conf['/myhouse/room#bed1/light#0.level']) != (0) , '/myhouse/room#bed1/light#0.level', 5),
	(lambda cont,conf:(conf['/myhouse/room#bed1/ac#0.level']) > (0) , '/myhouse/room#bed1/ac#0.level', 9),
	(lambda cont,conf: (cont['/myhouse/room#bed2.air'] ) > (6) and (cont['/myhouse.outtemp'] ) >= (10)  , '/myhouse/room#bed2/window#w1.opened', True),
	(lambda cont,conf: (cont['/myhouse/room#bed2.temp'] ) < (10) and (cont['/myhouse.eprice'] ) < (20)  , '/myhouse/room#bed2/heating#h.level', 10),
	(lambda cont,conf:(conf['/myhouse/room#bed2/light#0.level']) != (0) , '/myhouse/room#bed2/light#0.level', 5),
	(lambda cont,conf:(conf['/myhouse/room#bed2/ac#0.level']) > (0) , '/myhouse/room#bed2/ac#0.level', 9),
	(lambda cont,conf:conf['/myhouse/room#family/projector.on'] , '/myhouse/room#family/window#w2.curtainOn', True),
	(lambda cont,conf: (cont['/myhouse/room#family.air'] ) > (6) and (cont['/myhouse.outtemp'] ) >= (10)  , '/myhouse/room#family/window#w2.opened', True),
	(lambda cont,conf: (cont['/myhouse/room#family.temp'] ) < (10) and (cont['/myhouse.eprice'] ) < (20)  , '/myhouse/room#family/heating#h1.level', 10),
	(lambda cont,conf:(conf['/myhouse/room#family/light#0.level']) != (0) , '/myhouse/room#family/light#0.level', 5),
	(lambda cont,conf:(conf['/myhouse/room#family/ac#0.level']) > (0) , '/myhouse/room#family/ac#0.level', 9),
	(lambda cont,conf:cont['/myhouse/room#family/wm.loaded']  , '/myhouse/room#family/wm.on', True),
	(lambda cont,conf: (cont['/myhouse/room#bed3.air'] ) > (6) and (cont['/myhouse.outtemp'] ) >= (10)  , '/myhouse/room#bed3/window#w1.opened', True),
	(lambda cont,conf: (cont['/myhouse/room#bed3.temp'] ) < (10) and (cont['/myhouse.eprice'] ) < (20)  , '/myhouse/room#bed3/heating#h.level', 10),
	(lambda cont,conf:(conf['/myhouse/room#bed3/light#0.level']) != (0) , '/myhouse/room#bed3/light#0.level', 5),
	(lambda cont,conf: (cont['/myhouse/room#bath1.temp'] ) < (10) and (cont['/myhouse.eprice'] ) < (20)  , '/myhouse/room#bath1/heating#h1.level', 10),
	(lambda cont,conf:(conf['/myhouse/room#bath1/light#0.level']) != (0) , '/myhouse/room#bath1/light#0.level', 5),
	(lambda cont,conf: (cont['/myhouse/wh.temp'] ) < (30) and  (cont['/myhouse.time'] ) < (2) or (cont['/myhouse.time'] ) > (8)   , '/myhouse/wh.on', True)
]

